COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BASL30\M1BASI30\M2NGR40L\.
C00007 ENDMK
C⊗;
\\M0BASL30;\M1BASI30;\M2NGR40L;\.
\F2\CSTANFORD ARTIFICIAL INTELLIGENCE LABORATORY
\CDEPARTMENT OF COMPUTER SCIENCE
\CSTANFORD UNIVERSITY
\CSTANFORD, CALIFORNIA 94305
\F0
						December 17, 1973

Professor Shigeru Igarashi
Research Institute for Mathematical Sciences
Kyoto University
Kitashirakawa, Kyoto, Japan


Dear Shigeru,

\J	Thanks for your letter of November 15.  Coming to Japan for my
sabbatical is one of the major possibilities I would like to consider.
I would be able to commit myself in early fall 1974 and the period of
interest is nine months during the period June 1974 to September 1975.
It seems to me now that if I do come to Japan, the exact dates wouldn't
matter to me and therefore could be adjusted to fit the Japanese academic
calendar.

	I did some thinking last Spring about axiomatizing Scott theory
in first order logic.  I have not yet fully understood your AI memo on
the subject, but I have introduced a notion of \F1extensional form\F0
which may help with your or other axiomatization of the theory. 
An extensional form is a cross between a function and a form.  Like a
form, it has free variables, but like functions it is extensional in
that two forms are the same if they have the same values for the same
values of the variables.  Thus if + is a commutative functional constant,
then \F1x\F0+\F1y\F0 and \F1y\F0+\F1x\F0 are the same extensional form.

	I enclose a listing of a set of axioms for extensional forms.
They are for Weyhrauch's FOL and presuppose a suitable set theory.
There is one feature of the axioms that I now think I will change.  With
the present axioms \F1x\F0+\F1y\F0 is the same form regarded as a form in
\F1x\F0 and \F1y\F0 or regarded as a form in \F1x, y\F0 and \F1z\F0.
It looks better to regard them as different.

	The next step I intended was to introduce continuous functions
and the corresponding forms and add some version of your axioms, but I
encountered some difficulties the exact nature of which I forget.  Perhaps
this approach will be of some use to you.

	Malcolm Newey undertook to prove LCOM0 correct using LCF, but he
did not finally succeed.  In my opinion, one of the sources of his troubles
was that LCF doesn't admit proper quantifiers and negation, and this makes
it even more desirable to get Scott logic properly imbedded in first order logic.

	Is there any chance of your coming by Stanford on your way
to or from Nice?  We could pay the part of your expenses represented by
travel within the U.S. if that would help.\.

						Best Regards,


						John McCarthy
						Professor of Computer Science
						Director, Artificial Intelligence Laboratory.